$\forall$$A$:Type, $X$:MaInterface($A$), ${\it es}$:ES. \\[0ex]ma{-}interface{-}consistent(${\it es}$;$X$) $\Rightarrow$ ([[$X$]] $\in$ AbsInterface($A$))